PRISM
=====
Version: 4.5.dev
Date: Sat Mar 14 16:29:25 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -ii -e 5e-2 -heuristic speed -ddextraactionvars 100 -maxiters 1000000 consensus.6.prism consensus.props --property steps_min -const K=2
Parsing model file "consensus.6.prism"...
Type: MDP
Modules: process1 process2 process3 process4 process5 process6
Variables: counter pc1 coin1 pc2 coin2 pc3 coin3 pc4 coin4 pc5 coin5 pc6 coin6
Parsing properties file "consensus.props"...
5 properties:
(1) "c1": P>=1 [ F "finished" ]
(2) "c2": Pmin=? [ F "finished"&"all_coins_equal_1" ]
(3) "disagree": Pmax=? [ F "finished"&!"agree" ]
(4) "steps_max": R{"steps"}max=? [ F "finished" ]
(5) "steps_min": R{"steps"}min=? [ F "finished" ]
---------------------------------------------------------------------
Model checking: "steps_min": R{"steps"}min=? [ F "finished" ]
Model constants: K=2
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Warning: Switching to explicit engine to allow interval iteration on Rmin operator.
Building model...
Model constants: K=2
Computing reachable states... 190813 450814 714112 998339 1258240 states
Reachable states exploration and model construction done in 14.256 secs.
Sorting reachable states list...
Time for model construction: 17.94 seconds.
Type: MDP
States: 1258240 (1 initial)
Transitions: 6236736
Choices: 5008128
Max/avg: 6/3.98
Building reward structure...
Starting expected reachability (min)...
Starting Prob1 (max)...
Prob1 (max) took 49 iterations and 3.461 seconds.
target=384, inf=0, rest=1257856
For Rmin, checking for zero-reward ECs...
Time for checking for zero-reward ECs: 0.258 seconds, no zero-reward ECs found, proceeding normally.
Computing upper bound(s) for Rmin using the Dijkstra Sweep for Monotone Pessimistic Initialization algorithm...
Calculating incoming choices relation for Markov decision process... done (0.578 seconds)
Time for computing upper bound(s) for Rmin using the DSI-MP algorithm: 7.205 seconds.
Upper bound for min expectation (Dijkstra Sweep MPI): 18438.0
Starting Prob1 (min)...
Prob1 (min) took 64 iterations and 4.419 seconds.
Relevant sub-MDP is contracting, proceed...
Starting interval iteration (min, with Power method)...
Iteration 29: max relative diff=634.793103448, 5.14 sec so far
Iteration 59: max relative diff=311.24510372, 10.20 sec so far
Iteration 89: max relative diff=201.713556015, 15.22 sec so far
Iteration 119: max relative diff=144.618513, 20.25 sec so far
Iteration 149: max relative diff=109.806184634, 25.27 sec so far
Iteration 179: max relative diff=86.6562509556, 30.32 sec so far
Iteration 209: max relative diff=70.3208793259, 35.35 sec so far
Iteration 239: max relative diff=58.2731822398, 40.37 sec so far
Iteration 269: max relative diff=49.0773614434, 45.40 sec so far
Iteration 299: max relative diff=41.8638769614, 50.42 sec so far
Iteration 329: max relative diff=36.0788808003, 55.44 sec so far
Iteration 359: max relative diff=31.3546382223, 60.48 sec so far
Iteration 389: max relative diff=27.4382683047, 65.51 sec so far
Iteration 419: max relative diff=24.1505589105, 70.57 sec so far
Iteration 449: max relative diff=21.3611505371, 75.59 sec so far
Iteration 479: max relative diff=18.9730372803, 80.62 sec so far
Iteration 509: max relative diff=16.9125777537, 85.64 sec so far
Iteration 539: max relative diff=15.1228751247, 90.68 sec so far
Iteration 569: max relative diff=13.5592791987, 95.70 sec so far
Iteration 599: max relative diff=12.186261105, 100.72 sec so far
Iteration 629: max relative diff=10.9751974146, 105.74 sec so far
Iteration 659: max relative diff=9.90277010171, 110.79 sec so far
Iteration 689: max relative diff=8.94979190242, 115.81 sec so far
Iteration 719: max relative diff=8.10033089234, 120.92 sec so far
Iteration 749: max relative diff=7.34104904396, 125.94 sec so far
Iteration 779: max relative diff=6.66069614621, 130.97 sec so far
Iteration 809: max relative diff=6.04971810659, 135.99 sec so far
Iteration 839: max relative diff=5.49995055053, 141.02 sec so far
Iteration 869: max relative diff=5.00437678303, 146.05 sec so far
Iteration 899: max relative diff=4.55693484883, 151.17 sec so far
Iteration 929: max relative diff=4.15236242754, 156.20 sec so far
Iteration 959: max relative diff=3.78607115926, 161.23 sec so far
Iteration 989: max relative diff=3.45404406446, 166.25 sec so far
Iteration 1019: max relative diff=3.15275123502, 171.28 sec so far
Iteration 1049: max relative diff=2.87908009151, 176.30 sec so far
Iteration 1079: max relative diff=2.63027733728, 181.42 sec so far
Iteration 1109: max relative diff=2.40390036893, 186.45 sec so far
Iteration 1139: max relative diff=2.1977763809, 191.48 sec so far
Iteration 1169: max relative diff=2.00996776857, 196.51 sec so far
Iteration 1199: max relative diff=1.83874271696, 201.54 sec so far
Iteration 1229: max relative diff=1.68255008221, 206.56 sec so far
Iteration 1259: max relative diff=1.53999784525, 211.62 sec so far
Iteration 1289: max relative diff=1.40983455291, 216.64 sec so far
Iteration 1319: max relative diff=1.29093326921, 221.66 sec so far
Iteration 1349: max relative diff=1.18227764543, 226.68 sec so far
Iteration 1379: max relative diff=1.08294978647, 231.71 sec so far
Iteration 1409: max relative diff=0.992119646331, 236.74 sec so far
Iteration 1439: max relative diff=0.909035730629, 241.80 sec so far
Iteration 1469: max relative diff=0.833016920459, 246.82 sec so far
Iteration 1499: max relative diff=0.763445261999, 251.85 sec so far
Iteration 1529: max relative diff=0.699759590705, 256.87 sec so far
Iteration 1559: max relative diff=0.641449879203, 261.89 sec so far
Iteration 1589: max relative diff=0.588052214817, 266.92 sec so far
Iteration 1619: max relative diff=0.539144326547, 271.95 sec so far
Iteration 1649: max relative diff=0.494341593008, 276.97 sec so far
Iteration 1679: max relative diff=0.453293472532, 282.00 sec so far
Iteration 1709: max relative diff=0.415680304886, 287.03 sec so far
Iteration 1739: max relative diff=0.38121044091, 292.06 sec so far
Iteration 1769: max relative diff=0.349617662276, 297.09 sec so far
Iteration 1799: max relative diff=0.320658858514, 302.13 sec so far
Iteration 1829: max relative diff=0.294111932674, 307.15 sec so far
Iteration 1859: max relative diff=0.269773910633, 312.17 sec so far
Iteration 1889: max relative diff=0.247459232126, 317.30 sec so far
Iteration 1919: max relative diff=0.226998204274, 322.33 sec so far
Iteration 1949: max relative diff=0.208235600653, 327.36 sec so far
Iteration 1979: max relative diff=0.191029390958, 332.39 sec so far
Iteration 2009: max relative diff=0.175249588019, 337.41 sec so far
Iteration 2039: max relative diff=0.16077720044, 342.46 sec so far
Iteration 2069: max relative diff=0.147503280431, 347.49 sec so far
Iteration 2099: max relative diff=0.135328057545, 352.52 sec so far
Iteration 2129: max relative diff=0.124160150042, 357.55 sec so far
Iteration 2159: max relative diff=0.113915846461, 362.68 sec so far
Iteration 2189: max relative diff=0.104518450783, 367.70 sec so far
Iteration 2219: max relative diff=0.095897685233, 372.72 sec so far
Iteration 2249: max relative diff=0.0879891453694, 377.74 sec so far
Iteration 2279: max relative diff=0.0807338026702, 382.80 sec so far
Iteration 2309: max relative diff=0.074077550275, 387.83 sec so far
Iteration 2339: max relative diff=0.0679707879798, 392.86 sec so far
Iteration 2369: max relative diff=0.0623680429584, 397.90 sec so far
Iteration 2399: max relative diff=0.0572276230194, 402.94 sec so far
Iteration 2429: max relative diff=0.0525112995111, 407.97 sec so far
Max relative diff between upper and lower bound on convergence: 0.0499830451792
Interval iteration (min, with Power method) took 2446 iterations, 30508233984 multiplications and 411.224 seconds.
Maximum finite value in solution vector at end of interval iteration: 454.64285964456843
Expected reachability took 426.678 seconds.
Value in the initial state: 442.2833022174809
Time for model checking: 427.47 seconds.
Result: 442.2833022174809 (value in the initial state)
Overall running time: 446.002 seconds.
---------------------------------------------------------------------
Note: There were 2 warnings during computation.